nLab Adjointness in Foundations

This page collects links related to the text

  • William Lawvere,

    Adjointness in Foundations,

    Dialectica 23 (1969), 281-296,

    Reprints in Theory and Applications of Categories, No. 16 (2006), pp 1-16 (revised 2006-10-30)

    (TAC)

on foundations of mathematics in categorical logic and the role of adjoints in the formalization of quantifiers (base change). The main point is that the logical operations on propositions

existential quantifier\dashv context extension \dashv universal quantifier

constitute an adjoint triple. In type theory this is lifted from operations on propositions to operations on types, where it becomes

dependent sum\dashv context extension \dashv dependent product.

In topos theory and geometry this adjoint triple is often known as base change.

category: reference

Last revised on May 24, 2023 at 21:11:01. See the history of this page for a list of all contributions to it.